| Definitions | Void, t  T,  x:A. B(x), Top,  x:A. B(x), P & Q, True, locl(a), KindDeq, Knd, eqof(d), f(a), true ,  b,  A, b, x:A B(x), Prop, p  q, Type,  , s = t, false, False, left+right, P  Q, p q, x:A  B(x), P   Q, P  Q, P Q,  T, Unit, f(x), x dom(f), f(x)?z, , x : v, Id, a = b,  x. t(x), a:A fp B(a), State(ds),  x:A. B(x), Dec(P), Normal(ds), AtomFree(T;x), if b t else f fi, Normal(T), es realizer ind Rpre compseq tag def, Valtype(da;k), R-da(R;i), R-Feasible(R), lnk-decl(l;dt), f  g, 1of(t), type List, (x l), 2of(t), deq-member(eq;x;L), source(l), IdLnk, DeclaredType(ds;x), lnk(k), destination(l), tag(k), IdDeq, x.A(x), isrcv(k), es realizer ind Rsends compseq tag def, es realizer ind Reffect compseq tag def, Realizer, es realizer ind, A || B, x,y,z. t(x;y;z), x,y,z,w,v. t(x;y;z;w;v), x,y,z,u,v,w. t(x;y;z;u;v;w), x,y,z,w. t(x;y;z;w), es realizer ind Rplus compseq tag def, es realizer ind Rrframe compseq tag def, es realizer ind Rbframe compseq tag def, es realizer ind Raframe compseq tag def, es realizer ind Rsframe compseq tag def, es realizer ind Rframe compseq tag def, es realizer ind Rinit compseq tag def, es realizer ind Rnone compseq tag def, @loc: only members of L read x, @loc: k sends only on links in L, @loc: k writes only members of L, @loc precondition for a(v:T):P State(ds) v, sends knd(v:T) on l:tagged(g,State(ds),v):dt, @loc effect knd(v:T) x := f State(ds) v , only events in L send on lnk with tag, @loc only events in L change x:T, @loc x initially v:T, left right,  , {T}, , {x:A| B(x) }, x,y. t(x;y), xdom(f). v=f(x) P(x;v), SQType(T), s ~ t, rcv(l,tg), map(f;as) |
| Lemmas | member map, map wf, rcv wf, Knd sq, fpf-cap-single1, lnk-decl wf, fpf-single-dom, fpf-single wf, top wf, fpf-all wf, fpf-join-cap-sq, fpf-dom wf, fpf-trivial-subtype-top, es realizer-induction, Rnone wf, Rplus wf, ma-valtype wf, R-da wf, Rinit wf, Rframe wf, Rsframe wf, Reffect wf, Rsends wf, Rpre wf, Raframe wf, Rbframe wf, R-Feasible wf, Rrframe wf, normal-type wf, it wf, es realizer ind wf, R-compat wf, es realizer wf, isrcv wf, fpf-cap wf, id-deq wf, tagof wf, ldst wf, lnk wf, decl-type wf, IdLnk wf, lsrc wf, assert-deq-member, deq-member wf, l member wf, atom-free wf, normal-ds wf, decidable wf, decl-state wf, fpf wf, not functionality wrt iff, assert-eq-id, eq id wf, Id wf, eqtt to assert, assert of bor, eqff to assert, squash wf, bnot thru bor, iff transitivity, assert of band, and functionality wrt iff, assert of bnot, bor wf, false wf, bfalse wf, bool wf, band wf, bnot wf, not wf, assert wf, btrue wf, eqof wf, Knd wf, Kind-deq wf, locl wf, true wf |